module TravelDream

sig wString {}
sig Boolean { }

sig User
{
	id:one Int,
	username:one wString,
	email:one wString
}{
	id > 0
}

abstract sig Employee extends User
{

}

sig Administrator extends User
{
}

sig Customer extends User
{
}

sig Package
{
	id: one Int,
	packCreatorId: one Employee,
	packStart: one Int,
	packEnd:  one Int

}{
	id > 0
	packStart < packEnd
}

sig CustomPackage
{
	id: one Int,
	cPackCreator: one Customer,
	packageLink: one Package,
	packProduct: set BasicProduct,
	gift: one Boolean,
	purchased: one Boolean
}{
	id > 0	 
}

abstract sig BasicProduct
{
	id: one Int,
}{
	id > 0
}

sig Flight extends BasicProduct{
	depDate: one Int,
	arrivalDate: one Int
}{
	depDate < arrivalDate
}

sig Hotel extends BasicProduct{ 
	cost: one Int,
	checkinDate: one Int,
	checkoutDate: one Int
}{ 
	cost > 0
	checkinDate < checkoutDate
}

sig Excursion extends BasicProduct{ 
	start: one Int,
	end: one Int,
	cost: one Int 
}{ 
	cost >= 0
	start < end	
}

//************
//Facts
//************

//-----------------------UNIQUENESS OF IDs
fact NoDuplicateId{
    no disj u1,u2: User | u1.id=u2.id
	no disj bp1, bp2: BasicProduct | bp1.id = bp2.id
	no disj p1, p2: Package | p1.id = p2.id
	no disj cp1, cp2: CustomPackage | cp1.id = cp2.id
}
assert A_NoDuplicateId{
    no disj u1,u2: User | u1.id=u2.id
	no disj bp1, bp2: BasicProduct | bp1.id = bp2.id
	no disj p1, p2: Package | p1.id = p2.id
	no disj cp1, cp2: CustomPackage | cp1.id = cp2.id
}
check A_NoDuplicateId for 4
//---------------------- THE SYSTEM HAS ONE ADMINISTRATOR
fact OneAdmin {
#Administrator = 1
}

//---------------------- NO DUPLICATE USER
fact NoDuplicateUser {
	no disj u1, u2 : User | u1.username = u2.username || u1.email = u2.email
}

assert A_NoDuplicateUser{
    no disj u1, u2: User | u1.username=u2.username || u1.email=u2.email
}

check A_NoDuplicateUser for 4


//************
//Predicates
//************

//add basic product to custom package

pred show()
{
	#Employee = 1
    #Customer = 2
	#Package = 1
	#CustomPackage = 2
	#BasicProduct = 3
	
}


run show for 5 

pred addBasicProductToPackage(cp,cp':CustomPackage, bp:BasicProduct)
{
	not bp in cp.packProduct
	cp'.packProduct = cp.packProduct + bp

}

run addBasicProductToPackage for 3 but 2 CustomPackage


pred addProductToCustomPackage(cp, cp': CustomPackage,  c: BasicProduct){
	//postcondition
	cp'.packProduct = cp.packProduct + c  
}

run  addProductToCustomPackage  

